The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(s(N)))
sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))
dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))
add(0, X) → X
add(s(X), Y) → s(add(X, Y))
first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z)))
terms(X) → n__terms(X)
first(X1, X2) → n__first(X1, X2)
activate(n__terms(X)) → terms(X)
activate(n__first(X1, X2)) → first(X1, X2)
activate(X) → X

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^3).


The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(s(N))) [1]
sqr(0) → 0 [1]
sqr(s(X)) → s(add(sqr(X), dbl(X))) [1]
dbl(0) → 0 [1]
dbl(s(X)) → s(s(dbl(X))) [1]
add(0, X) → X [1]
add(s(X), Y) → s(add(X, Y)) [1]
first(0, X) → nil [1]
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) [1]
terms(X) → n__terms(X) [1]
first(X1, X2) → n__first(X1, X2) [1]
activate(n__terms(X)) → terms(X) [1]
activate(n__first(X1, X2)) → first(X1, X2) [1]
activate(X) → X [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

terms(N) → cons(recip(sqr(N)), n__terms(s(N))) [1]
sqr(0) → 0 [1]
sqr(s(X)) → s(add(sqr(X), dbl(X))) [1]
dbl(0) → 0 [1]
dbl(s(X)) → s(s(dbl(X))) [1]
add(0, X) → X [1]
add(s(X), Y) → s(add(X, Y)) [1]
first(0, X) → nil [1]
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) [1]
terms(X) → n__terms(X) [1]
first(X1, X2) → n__first(X1, X2) [1]
activate(n__terms(X)) → terms(X) [1]
activate(n__first(X1, X2)) → first(X1, X2) [1]
activate(X) → X [1]

The TRS has the following type information:

terms :: s:0 → n__terms:cons:nil:n__first cons :: recip → n__terms:cons:nil:n__first → n__terms:cons:nil:n__first recip :: s:0 → recip sqr :: s:0 → s:0 n__terms :: s:0 → n__terms:cons:nil:n__first s :: s:0 → s:0 0 :: s:0 add :: s:0 → s:0 → s:0 dbl :: s:0 → s:0 first :: s:0 → n__terms:cons:nil:n__first → n__terms:cons:nil:n__first nil :: n__terms:cons:nil:n__first n__first :: s:0 → n__terms:cons:nil:n__first → n__terms:cons:nil:n__first activate :: n__terms:cons:nil:n__first → n__terms:cons:nil:n__first

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

terms
first
activate

(c) The following functions are completely defined:

sqr
dbl
add

Due to the following rules being added:
none

And the following fresh constants:

const

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: terms(N) → cons(recip(sqr(N)), n__terms(s(N))) [1] sqr(0) → 0 [1] sqr(s(X)) → s(add(sqr(X), dbl(X))) [1] dbl(0) → 0 [1] dbl(s(X)) → s(s(dbl(X))) [1] add(0, X) → X [1] add(s(X), Y) → s(add(X, Y)) [1] first(0, X) → nil [1] first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) [1] terms(X) → n__terms(X) [1] first(X1, X2) → n__first(X1, X2) [1] activate(n__terms(X)) → terms(X) [1] activate(n__first(X1, X2)) → first(X1, X2) [1] activate(X) → X [1] The TRS has the following type information: terms :: s:0 → n__terms:cons:nil:n__first cons :: recip → n__terms:cons:nil:n__first → n__terms:cons:nil:n__first recip :: s:0 → recip sqr :: s:0 → s:0 n__terms :: s:0 → n__terms:cons:nil:n__first s :: s:0 → s:0 0 :: s:0 add :: s:0 → s:0 → s:0 dbl :: s:0 → s:0 first :: s:0 → n__terms:cons:nil:n__first → n__terms:cons:nil:n__first nil :: n__terms:cons:nil:n__first n__first :: s:0 → n__terms:cons:nil:n__first → n__terms:cons:nil:n__first activate :: n__terms:cons:nil:n__first → n__terms:cons:nil:n__first const :: recip Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: terms(N) → cons(recip(sqr(N)), n__terms(s(N))) [1] sqr(0) → 0 [1] sqr(s(0)) → s(add(0, 0)) [3] sqr(s(s(X'))) → s(add(s(add(sqr(X'), dbl(X'))), s(s(dbl(X'))))) [3] dbl(0) → 0 [1] dbl(s(X)) → s(s(dbl(X))) [1] add(0, X) → X [1] add(s(X), Y) → s(add(X, Y)) [1] first(0, X) → nil [1] first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) [1] terms(X) → n__terms(X) [1] first(X1, X2) → n__first(X1, X2) [1] activate(n__terms(X)) → terms(X) [1] activate(n__first(X1, X2)) → first(X1, X2) [1] activate(X) → X [1] The TRS has the following type information: terms :: s:0 → n__terms:cons:nil:n__first cons :: recip → n__terms:cons:nil:n__first → n__terms:cons:nil:n__first recip :: s:0 → recip sqr :: s:0 → s:0 n__terms :: s:0 → n__terms:cons:nil:n__first s :: s:0 → s:0 0 :: s:0 add :: s:0 → s:0 → s:0 dbl :: s:0 → s:0 first :: s:0 → n__terms:cons:nil:n__first → n__terms:cons:nil:n__first nil :: n__terms:cons:nil:n__first n__first :: s:0 → n__terms:cons:nil:n__first → n__terms:cons:nil:n__first activate :: n__terms:cons:nil:n__first → n__terms:cons:nil:n__first const :: recip Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
nil => 0
const => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ X :|: X >= 0, z = X
activate(z) -{ 1 }→ terms(X) :|: z = 1 + X, X >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ X :|: z' = X, X >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(X, Y) :|: z = 1 + X, z' = Y, Y >= 0, X >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(X)) :|: z = 1 + X, X >= 0
first(z, z') -{ 1 }→ 0 :|: z' = X, X >= 0, z = 0
first(z, z') -{ 1 }→ 1 + X1 + X2 :|: X1 >= 0, X2 >= 0, z = X1, z' = X2
first(z, z') -{ 1 }→ 1 + Y + (1 + X + activate(Z)) :|: Z >= 0, z = 1 + X, Y >= 0, X >= 0, z' = 1 + Y + Z
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(X'), dbl(X')), 1 + (1 + dbl(X'))) :|: X' >= 0, z = 1 + (1 + X')
terms(z) -{ 1 }→ 1 + X :|: X >= 0, z = X
terms(z) -{ 1 }→ 1 + (1 + sqr(N)) + (1 + (1 + N)) :|: z = N, N >= 0

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(12) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ dbl } { add } { sqr } { terms } { first, activate }

(14) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {sqr}, {terms}, {first,activate}

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2·z

(16) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {dbl}, {add}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: ?, size: O(n1) [2·z]

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: dbl
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(18) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 }→ 1 + (1 + dbl(z - 1)) :|: z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 3 }→ 1 + add(1 + add(sqr(z - 2), dbl(z - 2)), 1 + (1 + dbl(z - 2))) :|: z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z]

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(20) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z]

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(22) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {add}, {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: ?, size: O(n1) [z + z']

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: add
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(24) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 }→ 1 + add(z - 1, z') :|: z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 3 }→ 1 + add(0, 0) :|: z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 1 + 4·z + 4·z²

(28) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {sqr}, {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: ?, size: O(n2) [1 + 4·z + 4·z2]

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: sqr
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 5 + 22·z + 8·z³

(30) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ 1 + 2·z }→ 1 + add(1 + add(sqr(z - 2), s), 1 + (1 + s')) :|: s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 1 }→ 1 + (1 + sqr(z)) + (1 + (1 + z)) :|: z >= 0

Function symbols to be analyzed: {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2]

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(32) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s3) + (1 + (1 + z)) :|: s3 >= 0, s3 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2]

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 6 + 6·z + 4·z²

(34) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s3) + (1 + (1 + z)) :|: s3 >= 0, s3 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {terms}, {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: ?, size: O(n2) [6 + 6·z + 4·z2]

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: terms
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 7 + 22·z + 8·z³

(36) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ terms(z - 1) :|: z - 1 >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s3) + (1 + (1 + z)) :|: s3 >= 0, s3 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: O(n3) [7 + 22·z + 8·z3], size: O(n2) [6 + 6·z + 4·z2]

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(38) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ -22 + 46·z + -24·z² + 8·z³ }→ s7 :|: s7 >= 0, s7 <= 6 * (z - 1) + 4 * ((z - 1) * (z - 1)) + 6, z - 1 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s3) + (1 + (1 + z)) :|: s3 >= 0, s3 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: O(n3) [7 + 22·z + 8·z3], size: O(n2) [6 + 6·z + 4·z2]

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

Computed SIZE bound using CoFloCo for: activate
after applying outer abstraction to obtain an ITS,
resulting in: INF with polynomial bound: ?

(40) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ -22 + 46·z + -24·z² + 8·z³ }→ s7 :|: s7 >= 0, s7 <= 6 * (z - 1) + 4 * ((z - 1) * (z - 1)) + 6, z - 1 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s3) + (1 + (1 + z)) :|: s3 >= 0, s3 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed: {first,activate}
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: O(n3) [7 + 22·z + 8·z3], size: O(n2) [6 + 6·z + 4·z2] first: runtime: ?, size: INF activate: runtime: ?, size: INF

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 3 + 48·z' + 8·z'³

Computed RUNTIME bound using KoAT for: activate
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 5 + 94·z + 16·z³

(42) Obligation:

Complexity RNTS consisting of the following rules:

activate(z) -{ -22 + 46·z + -24·z² + 8·z³ }→ s7 :|: s7 >= 0, s7 <= 6 * (z - 1) + 4 * ((z - 1) * (z - 1)) + 6, z - 1 >= 0
activate(z) -{ 1 }→ z :|: z >= 0
activate(z) -{ 1 }→ first(X1, X2) :|: X1 >= 0, X2 >= 0, z = 1 + X1 + X2
add(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
add(z, z') -{ 1 + z }→ 1 + s2 :|: s2 >= 0, s2 <= 1 * (z - 1) + 1 * z', z' >= 0, z - 1 >= 0
dbl(z) -{ 1 }→ 0 :|: z = 0
dbl(z) -{ 1 + z }→ 1 + (1 + s'') :|: s'' >= 0, s'' <= 2 * (z - 1), z - 1 >= 0
first(z, z') -{ 1 }→ 0 :|: z' >= 0, z = 0
first(z, z') -{ 1 }→ 1 + Y + (1 + (z - 1) + activate(Z)) :|: Z >= 0, Y >= 0, z - 1 >= 0, z' = 1 + Y + Z
first(z, z') -{ 1 }→ 1 + z + z' :|: z >= 0, z' >= 0
sqr(z) -{ 1 }→ 0 :|: z = 0
sqr(z) -{ 4 }→ 1 + s1 :|: s1 >= 0, s1 <= 1 * 0 + 1 * 0, z = 1 + 0
sqr(z) -{ -99 + s4 + s5 + 120·z + -48·z² + 8·z³ }→ 1 + s6 :|: s4 >= 0, s4 <= 4 * ((z - 2) * (z - 2)) + 4 * (z - 2) + 1, s5 >= 0, s5 <= 1 * s4 + 1 * s, s6 >= 0, s6 <= 1 * (1 + s5) + 1 * (1 + (1 + s')), s >= 0, s <= 2 * (z - 2), s' >= 0, s' <= 2 * (z - 2), z - 2 >= 0
terms(z) -{ 1 }→ 1 + z :|: z >= 0
terms(z) -{ 6 + 22·z + 8·z³ }→ 1 + (1 + s3) + (1 + (1 + z)) :|: s3 >= 0, s3 <= 4 * (z * z) + 4 * z + 1, z >= 0

Function symbols to be analyzed:
Previous analysis results are:

dbl: runtime: O(n1) [1 + z], size: O(n1) [2·z] add: runtime: O(n1) [1 + z], size: O(n1) [z + z'] sqr: runtime: O(n3) [5 + 22·z + 8·z3], size: O(n2) [1 + 4·z + 4·z2] terms: runtime: O(n3) [7 + 22·z + 8·z3], size: O(n2) [6 + 6·z + 4·z2] first: runtime: O(n3) [3 + 48·z' + 8·z'3], size: INF activate: runtime: O(n3) [5 + 94·z + 16·z3], size: INF

(43) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(44) BOUNDS(1, n^3)